\documentclass{article}

\usepackage{geometry}
\usepackage{latexsym}
\usepackage[pdftex]{graphicx}
\usepackage{subfigure}   %Deals with subfigures
\usepackage{fancyhdr}
\usepackage{hyperref}
\usepackage{courier}    
\usepackage{listings}
\usepackage{verbatim} 
\usepackage{eurosym}                                                                                                          
\geometry{a4paper,left=30mm,right=25mm,top=25mm,bottom=30mm} 
\pagestyle{fancy}

\lstset{
  showspaces=false, %Leaves spaces blank
  showstringspaces=false, %Leaves spaces in strings blank
  breaklines=true, %Break lines that are too long
  basicstyle=\ttfamily\small, %The text style and size of the code 
  extendedchars=true, %Includes danish characters 
  numbers = left, %Shows linenumbers
  stepnumber = 1, %The interval with which linenumbers are displayed
  numberstyle=\footnotesize %The label size 
}

\begin{document}

\begin{titlepage}
\thispagestyle{fancy}
\lhead{}
\chead{
\large{\textit{
Informatics and Mathematical Modelling\\
Technical University of Denmark}}}
\rhead{}
\rule{0pt}{50pt}
\vspace{3cm}

\begin{center}
{\huge Introduction to Robust Programming\\
and Spec\#\\}
\vspace{2cm}
\LARGE{02241 Robust Programming in .NET}\\
\Large{Fall 2007}\\
\Large{Assignment 1}\\
[36ex]}
\end{center}
\begin{flushright}
\Large{s053739 Markku Eerola}\\
\vspace{1cm}
\Large{s061332 Rajesh Bachani}\\
\vspace{1cm}
\Large{s071312 Jakob Jensen}\\
[3ex]
\end{flushright}%}
\vfill
\rule{0pt}{0pt}
\cfoot{\today}
\end{titlepage}

\lhead{}             
\chead{}
\rhead{\footnotesize \thepage }
\lfoot{}
\cfoot{}
\rfoot{}

\newpage

\section{Robust Programming}

The state of the art in software and hardware are usually compared together. While, we have advanced heavily in the hardware paradigm, with high computational speeds and thus high capabilities, software seems to be having its problems. Very commonly, software is fragile and contains errors. Successful software engineering is based on the quality of the software delivered in terms of software abiding by some given specifications. The entire engineering process could be considered flawed if there is no full compliance between the expected outcome (as from the design) and the actual outcome (the software) from this process of engineering. Robust programming, though just a small part of this entire process, is very important, as it ensures that the software does not behave in any abnormal or unpredictable way.\\

The high complexity of software programs these days make it complex to efficiently identify errors, ultimately leading to \textit{buggy} code \cite{2}. For example, there could be errors in the program that become visible only under certain circumstances while running. These could be related with some abnormal behavior associated with dependencies like memory routines or networking functions etc. Another common instance which leads to software failures is during its interaction with the user. Since software directly interacts with users, and could have all sorts of inputs (as opposed to just digital values in hardware), it is difficult to identify the various possible invalid inputs that could be posted to the program and that should be dealt with reasonably.\\

The case of invalid inputs could occur within routine calls as well, when a parameter passed by a caller routine is not recognised by the callee routine, and the callee does not know how to deal with it. The result of this execution could be a complete crash of the system or some unexpected result being returned to the caller and cascaded back to the user in some form. As can be understood in such case, the result sent to the user, could literally be anything \textit{unpredictable}. There is a notion of uncertainty as to how the program would behave in such situations, and this is what is not wanted at all in any sort of programs.\\

Software developers need to always make sure that the software performs the required job, and deals intelligently in every possible situation. Assumptions regarding the program should be carefully sketched, such that they hold in all circumstances and are not violated by user inputs or any particular internal behavior. Assumptions which might cease to hold in certain cases can be problematic leading to such unpredictable outcomes.\\

In general, program errors could occur due to any of the following reasons, as mentioned in \cite{3}:
\begin{itemize}
\item \textit{Compile time errors} occur as a result of syntactical mismatch of the program with the language specifications.
\item \textit{Run time program errors} result from internal errors, such as a null pointer accessing data, or array index being negative. Recovery from these errors is impossible and the program has to notify the user and terminate.
\item \textit{Run time user errors} result from user inputs which are not recognised by the program.
\item \textit{Run time exceptions} are internal error situations which can be handled by the program to some extent.
\end{itemize}\\

Robust programs deal with the last three kinds of errors occuring at runtime. A program is robust if the program does not show any abnormal output or behavior and it performs exactly as it is designed to. For valid user inputs, the program should perform the desired valid action, while for invalid user inputs, it must either exit gracefully or prompt the user to enter valid values, or perform any other reasonable action. Internal errors could occur, and the program must provide the user enough information on the reason for the error which may be helpful in debugging the program. These are the cases which we have discussed in the intial paragraphs of the section.\\

Robustness is necessary to ensure the safety of any system that consists of a software controller. In complex systems which incorporate strong interaction between hardware and software, any unpredictable result from the software could yield the hardware create havoc. For example, the failure of the Ariane 5 Flight 501, resulted from a software malfunction, which led the rocket to self-destruct in just 37 seconds of its flight. This was considered one of the most expensive software bug in history. There have been other system failures due to unpredictable software component, which has affected human lives also.\\

Other major consequence that non-robust programs could lead to is the security of the software. Attackers could intelligently take advantage of the bugs in software to gain control of the system, and perform unauthentic actions. Buffer overflow bugs which are infamous for creating a majority of vulnerabilities in softwares, occur if the user inputs are not validated. Validating user inputs for sanity is integral to robust programming, and if such a practice is ignored, security risks could very well be raised.

\section{Spec\#}

The Spec\# programming system developed by Microsoft is intended to provide programmers with means to improve the correctness of the programs they write thus promoting robustness. The system is integrated on the existing .NET platform to make it more easily adoptable. It consists of Spec\# language, which is an extension to the object-oriented .NET programming language C\#, a Spec\# compiler and an automatic program verifier codenamed Boogie \cite{4}.\\

Spec\# language's main contribution to robust programming is adding annotations that allow the programmer to distinguish between expressions that may evaluate as null and expressions that will never evaluate as null, to specify pre- and post-conditions to methods that have to be met and to constrain data fields of objects.\\

Where Spec\# programming system really shines is that it includes both compiletime and runtime checking. This means that many errors that might've otherwise caused unexpected behavior or abnormal exits can be caught during compilation. Not only does this decrease the amount of errors in the end product but it also increases the efficiency of the program because things that can be checked during compilation do not need to be checked again runtime.\\

While the additions made to C\# by Spec\# sound good and are definitely welcome they don't automatically mean that using Spec# will increase robustness. The language cannot for example eradicate null-dereference errors on its own. The tool is only as good as its user. If the programmer doesn't exploit the new features using the language does not guarantee correctness.\\

Still, it's obvious that having the tools will make it easier to promote correctness especially within a larger project. Example: Alice writes her methods using the pre- and post-conditions to ensure that when Bob calls her methods he is forced to do so with correct arguments. Because of this Bob cannot cause unexpected behavior within Alice's code.

\newpage
\nocite{1}
\bibliographystyle{plain}
\bibliography{RobustProgrammingAndSpecSharp}

\end{document}